(0) Obligation:
Clauses:
m(X, 0, Z) :- ','(!, =(Z, X)).
m(0, Y, Z) :- ','(!, =(Z, 0)).
m(X, Y, Z) :- ','(p(X, A), ','(p(Y, B), m(A, B, Z))).
p(0, 0).
p(s(0), 0).
p(s(s(X)), s(Y)) :- p(s(X), Y).
=(X, X).
Query: m(g,g,a)
(1) BuiltinConflictTransformerProof (EQUIVALENT transformation)
Renamed defined predicates conflicting with built-in predicates [PROLOG].
(2) Obligation:
Clauses:
m(X, 0, Z) :- ','(!, user_defined_=(Z, X)).
m(0, Y, Z) :- ','(!, user_defined_=(Z, 0)).
m(X, Y, Z) :- ','(p(X, A), ','(p(Y, B), m(A, B, Z))).
p(0, 0).
p(s(0), 0).
p(s(s(X)), s(Y)) :- p(s(X), Y).
user_defined_=(X, X).
Query: m(g,g,a)
(3) PrologToDTProblemTransformerProof (SOUND transformation)
Built DT problem from termination graph DT10.
(4) Obligation:
Triples:
pA(s(X1), s(X2)) :- pA(X1, X2).
mB(s(0), s(s(X1)), X2) :- pA(X1, X3).
mB(s(s(X1)), X2, X3) :- pA(X1, X4).
mB(s(s(X1)), s(s(X2)), X3) :- ','(pcA(X1, X4), pA(X2, X5)).
mB(s(s(X1)), X2, X3) :- ','(pcA(X1, X4), ','(pcD(X2, X5), mB(s(X4), X5, X3))).
Clauses:
pcA(0, 0).
pcA(s(X1), s(X2)) :- pcA(X1, X2).
mcB(X1, 0, X1).
mcB(0, X1, 0).
mcB(s(0), X1, 0) :- pcC(X1, 0).
mcB(s(0), X1, 0) :- pcC(X1, X2).
mcB(s(s(X1)), X2, X3) :- ','(pcA(X1, X4), ','(pcD(X2, X5), mcB(s(X4), X5, X3))).
pcC(s(0), 0).
pcC(s(s(X1)), s(X2)) :- pcA(X1, X2).
pcD(s(0), 0).
pcD(s(s(X1)), s(X2)) :- pcA(X1, X2).
Afs:
mB(x1, x2, x3) = mB(x1, x2)
(5) TriplesToPiDPProof (SOUND transformation)
We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
mB_in: (b,b,f)
pA_in: (b,f)
pcA_in: (b,f)
pcD_in: (b,f)
Transforming
TRIPLES into the following
Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:
MB_IN_GGA(s(0), s(s(X1)), X2) → U2_GGA(X1, X2, pA_in_ga(X1, X3))
MB_IN_GGA(s(0), s(s(X1)), X2) → PA_IN_GA(X1, X3)
PA_IN_GA(s(X1), s(X2)) → U1_GA(X1, X2, pA_in_ga(X1, X2))
PA_IN_GA(s(X1), s(X2)) → PA_IN_GA(X1, X2)
MB_IN_GGA(s(s(X1)), X2, X3) → U3_GGA(X1, X2, X3, pA_in_ga(X1, X4))
MB_IN_GGA(s(s(X1)), X2, X3) → PA_IN_GA(X1, X4)
MB_IN_GGA(s(s(X1)), s(s(X2)), X3) → U4_GGA(X1, X2, X3, pcA_in_ga(X1, X4))
U4_GGA(X1, X2, X3, pcA_out_ga(X1, X4)) → U5_GGA(X1, X2, X3, pA_in_ga(X2, X5))
U4_GGA(X1, X2, X3, pcA_out_ga(X1, X4)) → PA_IN_GA(X2, X5)
MB_IN_GGA(s(s(X1)), X2, X3) → U6_GGA(X1, X2, X3, pcA_in_ga(X1, X4))
U6_GGA(X1, X2, X3, pcA_out_ga(X1, X4)) → U7_GGA(X1, X2, X3, X4, pcD_in_ga(X2, X5))
U7_GGA(X1, X2, X3, X4, pcD_out_ga(X2, X5)) → U8_GGA(X1, X2, X3, mB_in_gga(s(X4), X5, X3))
U7_GGA(X1, X2, X3, X4, pcD_out_ga(X2, X5)) → MB_IN_GGA(s(X4), X5, X3)
The TRS R consists of the following rules:
pcA_in_ga(0, 0) → pcA_out_ga(0, 0)
pcA_in_ga(s(X1), s(X2)) → U10_ga(X1, X2, pcA_in_ga(X1, X2))
U10_ga(X1, X2, pcA_out_ga(X1, X2)) → pcA_out_ga(s(X1), s(X2))
pcD_in_ga(s(0), 0) → pcD_out_ga(s(0), 0)
pcD_in_ga(s(s(X1)), s(X2)) → U17_ga(X1, X2, pcA_in_ga(X1, X2))
U17_ga(X1, X2, pcA_out_ga(X1, X2)) → pcD_out_ga(s(s(X1)), s(X2))
The argument filtering Pi contains the following mapping:
mB_in_gga(
x1,
x2,
x3) =
mB_in_gga(
x1,
x2)
s(
x1) =
s(
x1)
0 =
0
pA_in_ga(
x1,
x2) =
pA_in_ga(
x1)
pcA_in_ga(
x1,
x2) =
pcA_in_ga(
x1)
pcA_out_ga(
x1,
x2) =
pcA_out_ga(
x1,
x2)
U10_ga(
x1,
x2,
x3) =
U10_ga(
x1,
x3)
pcD_in_ga(
x1,
x2) =
pcD_in_ga(
x1)
pcD_out_ga(
x1,
x2) =
pcD_out_ga(
x1,
x2)
U17_ga(
x1,
x2,
x3) =
U17_ga(
x1,
x3)
MB_IN_GGA(
x1,
x2,
x3) =
MB_IN_GGA(
x1,
x2)
U2_GGA(
x1,
x2,
x3) =
U2_GGA(
x1,
x3)
PA_IN_GA(
x1,
x2) =
PA_IN_GA(
x1)
U1_GA(
x1,
x2,
x3) =
U1_GA(
x1,
x3)
U3_GGA(
x1,
x2,
x3,
x4) =
U3_GGA(
x1,
x2,
x4)
U4_GGA(
x1,
x2,
x3,
x4) =
U4_GGA(
x1,
x2,
x4)
U5_GGA(
x1,
x2,
x3,
x4) =
U5_GGA(
x1,
x2,
x4)
U6_GGA(
x1,
x2,
x3,
x4) =
U6_GGA(
x1,
x2,
x4)
U7_GGA(
x1,
x2,
x3,
x4,
x5) =
U7_GGA(
x1,
x2,
x4,
x5)
U8_GGA(
x1,
x2,
x3,
x4) =
U8_GGA(
x1,
x2,
x4)
We have to consider all (P,R,Pi)-chains
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
(6) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
MB_IN_GGA(s(0), s(s(X1)), X2) → U2_GGA(X1, X2, pA_in_ga(X1, X3))
MB_IN_GGA(s(0), s(s(X1)), X2) → PA_IN_GA(X1, X3)
PA_IN_GA(s(X1), s(X2)) → U1_GA(X1, X2, pA_in_ga(X1, X2))
PA_IN_GA(s(X1), s(X2)) → PA_IN_GA(X1, X2)
MB_IN_GGA(s(s(X1)), X2, X3) → U3_GGA(X1, X2, X3, pA_in_ga(X1, X4))
MB_IN_GGA(s(s(X1)), X2, X3) → PA_IN_GA(X1, X4)
MB_IN_GGA(s(s(X1)), s(s(X2)), X3) → U4_GGA(X1, X2, X3, pcA_in_ga(X1, X4))
U4_GGA(X1, X2, X3, pcA_out_ga(X1, X4)) → U5_GGA(X1, X2, X3, pA_in_ga(X2, X5))
U4_GGA(X1, X2, X3, pcA_out_ga(X1, X4)) → PA_IN_GA(X2, X5)
MB_IN_GGA(s(s(X1)), X2, X3) → U6_GGA(X1, X2, X3, pcA_in_ga(X1, X4))
U6_GGA(X1, X2, X3, pcA_out_ga(X1, X4)) → U7_GGA(X1, X2, X3, X4, pcD_in_ga(X2, X5))
U7_GGA(X1, X2, X3, X4, pcD_out_ga(X2, X5)) → U8_GGA(X1, X2, X3, mB_in_gga(s(X4), X5, X3))
U7_GGA(X1, X2, X3, X4, pcD_out_ga(X2, X5)) → MB_IN_GGA(s(X4), X5, X3)
The TRS R consists of the following rules:
pcA_in_ga(0, 0) → pcA_out_ga(0, 0)
pcA_in_ga(s(X1), s(X2)) → U10_ga(X1, X2, pcA_in_ga(X1, X2))
U10_ga(X1, X2, pcA_out_ga(X1, X2)) → pcA_out_ga(s(X1), s(X2))
pcD_in_ga(s(0), 0) → pcD_out_ga(s(0), 0)
pcD_in_ga(s(s(X1)), s(X2)) → U17_ga(X1, X2, pcA_in_ga(X1, X2))
U17_ga(X1, X2, pcA_out_ga(X1, X2)) → pcD_out_ga(s(s(X1)), s(X2))
The argument filtering Pi contains the following mapping:
mB_in_gga(
x1,
x2,
x3) =
mB_in_gga(
x1,
x2)
s(
x1) =
s(
x1)
0 =
0
pA_in_ga(
x1,
x2) =
pA_in_ga(
x1)
pcA_in_ga(
x1,
x2) =
pcA_in_ga(
x1)
pcA_out_ga(
x1,
x2) =
pcA_out_ga(
x1,
x2)
U10_ga(
x1,
x2,
x3) =
U10_ga(
x1,
x3)
pcD_in_ga(
x1,
x2) =
pcD_in_ga(
x1)
pcD_out_ga(
x1,
x2) =
pcD_out_ga(
x1,
x2)
U17_ga(
x1,
x2,
x3) =
U17_ga(
x1,
x3)
MB_IN_GGA(
x1,
x2,
x3) =
MB_IN_GGA(
x1,
x2)
U2_GGA(
x1,
x2,
x3) =
U2_GGA(
x1,
x3)
PA_IN_GA(
x1,
x2) =
PA_IN_GA(
x1)
U1_GA(
x1,
x2,
x3) =
U1_GA(
x1,
x3)
U3_GGA(
x1,
x2,
x3,
x4) =
U3_GGA(
x1,
x2,
x4)
U4_GGA(
x1,
x2,
x3,
x4) =
U4_GGA(
x1,
x2,
x4)
U5_GGA(
x1,
x2,
x3,
x4) =
U5_GGA(
x1,
x2,
x4)
U6_GGA(
x1,
x2,
x3,
x4) =
U6_GGA(
x1,
x2,
x4)
U7_GGA(
x1,
x2,
x3,
x4,
x5) =
U7_GGA(
x1,
x2,
x4,
x5)
U8_GGA(
x1,
x2,
x3,
x4) =
U8_GGA(
x1,
x2,
x4)
We have to consider all (P,R,Pi)-chains
(7) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 9 less nodes.
(8) Complex Obligation (AND)
(9) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
PA_IN_GA(s(X1), s(X2)) → PA_IN_GA(X1, X2)
The TRS R consists of the following rules:
pcA_in_ga(0, 0) → pcA_out_ga(0, 0)
pcA_in_ga(s(X1), s(X2)) → U10_ga(X1, X2, pcA_in_ga(X1, X2))
U10_ga(X1, X2, pcA_out_ga(X1, X2)) → pcA_out_ga(s(X1), s(X2))
pcD_in_ga(s(0), 0) → pcD_out_ga(s(0), 0)
pcD_in_ga(s(s(X1)), s(X2)) → U17_ga(X1, X2, pcA_in_ga(X1, X2))
U17_ga(X1, X2, pcA_out_ga(X1, X2)) → pcD_out_ga(s(s(X1)), s(X2))
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
0 =
0
pcA_in_ga(
x1,
x2) =
pcA_in_ga(
x1)
pcA_out_ga(
x1,
x2) =
pcA_out_ga(
x1,
x2)
U10_ga(
x1,
x2,
x3) =
U10_ga(
x1,
x3)
pcD_in_ga(
x1,
x2) =
pcD_in_ga(
x1)
pcD_out_ga(
x1,
x2) =
pcD_out_ga(
x1,
x2)
U17_ga(
x1,
x2,
x3) =
U17_ga(
x1,
x3)
PA_IN_GA(
x1,
x2) =
PA_IN_GA(
x1)
We have to consider all (P,R,Pi)-chains
(10) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(11) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
PA_IN_GA(s(X1), s(X2)) → PA_IN_GA(X1, X2)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
PA_IN_GA(
x1,
x2) =
PA_IN_GA(
x1)
We have to consider all (P,R,Pi)-chains
(12) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(13) Obligation:
Q DP problem:
The TRS P consists of the following rules:
PA_IN_GA(s(X1)) → PA_IN_GA(X1)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(14) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- PA_IN_GA(s(X1)) → PA_IN_GA(X1)
The graph contains the following edges 1 > 1
(15) YES
(16) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
MB_IN_GGA(s(s(X1)), X2, X3) → U6_GGA(X1, X2, X3, pcA_in_ga(X1, X4))
U6_GGA(X1, X2, X3, pcA_out_ga(X1, X4)) → U7_GGA(X1, X2, X3, X4, pcD_in_ga(X2, X5))
U7_GGA(X1, X2, X3, X4, pcD_out_ga(X2, X5)) → MB_IN_GGA(s(X4), X5, X3)
The TRS R consists of the following rules:
pcA_in_ga(0, 0) → pcA_out_ga(0, 0)
pcA_in_ga(s(X1), s(X2)) → U10_ga(X1, X2, pcA_in_ga(X1, X2))
U10_ga(X1, X2, pcA_out_ga(X1, X2)) → pcA_out_ga(s(X1), s(X2))
pcD_in_ga(s(0), 0) → pcD_out_ga(s(0), 0)
pcD_in_ga(s(s(X1)), s(X2)) → U17_ga(X1, X2, pcA_in_ga(X1, X2))
U17_ga(X1, X2, pcA_out_ga(X1, X2)) → pcD_out_ga(s(s(X1)), s(X2))
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
0 =
0
pcA_in_ga(
x1,
x2) =
pcA_in_ga(
x1)
pcA_out_ga(
x1,
x2) =
pcA_out_ga(
x1,
x2)
U10_ga(
x1,
x2,
x3) =
U10_ga(
x1,
x3)
pcD_in_ga(
x1,
x2) =
pcD_in_ga(
x1)
pcD_out_ga(
x1,
x2) =
pcD_out_ga(
x1,
x2)
U17_ga(
x1,
x2,
x3) =
U17_ga(
x1,
x3)
MB_IN_GGA(
x1,
x2,
x3) =
MB_IN_GGA(
x1,
x2)
U6_GGA(
x1,
x2,
x3,
x4) =
U6_GGA(
x1,
x2,
x4)
U7_GGA(
x1,
x2,
x3,
x4,
x5) =
U7_GGA(
x1,
x2,
x4,
x5)
We have to consider all (P,R,Pi)-chains
(17) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(18) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MB_IN_GGA(s(s(X1)), X2) → U6_GGA(X1, X2, pcA_in_ga(X1))
U6_GGA(X1, X2, pcA_out_ga(X1, X4)) → U7_GGA(X1, X2, X4, pcD_in_ga(X2))
U7_GGA(X1, X2, X4, pcD_out_ga(X2, X5)) → MB_IN_GGA(s(X4), X5)
The TRS R consists of the following rules:
pcA_in_ga(0) → pcA_out_ga(0, 0)
pcA_in_ga(s(X1)) → U10_ga(X1, pcA_in_ga(X1))
U10_ga(X1, pcA_out_ga(X1, X2)) → pcA_out_ga(s(X1), s(X2))
pcD_in_ga(s(0)) → pcD_out_ga(s(0), 0)
pcD_in_ga(s(s(X1))) → U17_ga(X1, pcA_in_ga(X1))
U17_ga(X1, pcA_out_ga(X1, X2)) → pcD_out_ga(s(s(X1)), s(X2))
The set Q consists of the following terms:
pcA_in_ga(x0)
U10_ga(x0, x1)
pcD_in_ga(x0)
U17_ga(x0, x1)
We have to consider all (P,Q,R)-chains.
(19) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
MB_IN_GGA(s(s(X1)), X2) → U6_GGA(X1, X2, pcA_in_ga(X1))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(MB_IN_GGA(x1, x2)) = x1
POL(U10_ga(x1, x2)) = 1 + x2
POL(U17_ga(x1, x2)) = 0
POL(U6_GGA(x1, x2, x3)) = 1 + x3
POL(U7_GGA(x1, x2, x3, x4)) = 1 + x3
POL(pcA_in_ga(x1)) = x1
POL(pcA_out_ga(x1, x2)) = x2
POL(pcD_in_ga(x1)) = 0
POL(pcD_out_ga(x1, x2)) = 0
POL(s(x1)) = 1 + x1
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
pcA_in_ga(0) → pcA_out_ga(0, 0)
pcA_in_ga(s(X1)) → U10_ga(X1, pcA_in_ga(X1))
U10_ga(X1, pcA_out_ga(X1, X2)) → pcA_out_ga(s(X1), s(X2))
(20) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U6_GGA(X1, X2, pcA_out_ga(X1, X4)) → U7_GGA(X1, X2, X4, pcD_in_ga(X2))
U7_GGA(X1, X2, X4, pcD_out_ga(X2, X5)) → MB_IN_GGA(s(X4), X5)
The TRS R consists of the following rules:
pcA_in_ga(0) → pcA_out_ga(0, 0)
pcA_in_ga(s(X1)) → U10_ga(X1, pcA_in_ga(X1))
U10_ga(X1, pcA_out_ga(X1, X2)) → pcA_out_ga(s(X1), s(X2))
pcD_in_ga(s(0)) → pcD_out_ga(s(0), 0)
pcD_in_ga(s(s(X1))) → U17_ga(X1, pcA_in_ga(X1))
U17_ga(X1, pcA_out_ga(X1, X2)) → pcD_out_ga(s(s(X1)), s(X2))
The set Q consists of the following terms:
pcA_in_ga(x0)
U10_ga(x0, x1)
pcD_in_ga(x0)
U17_ga(x0, x1)
We have to consider all (P,Q,R)-chains.
(21) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.
(22) TRUE